Nuprl Lemma : decidable__equal_unit
11,40
postcript
pdf
x
,
y
:Unit. decidable((
x
=
y
))
latex
Definitions
t
T
,
Unit
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
A
,
P
Q
,
decidable(
P
)
,
Lemmas
it
wf
,
not
wf
,
unit
wf
origin
x,y:Unit. decidable((x = y)) x,y:Unit. decidable((x = y)) 
Tx:A. B(x)
A
Q